ePMC

Benchmark

Model:	consensus v.1 (MDP)
Parameter(s)	N = 4, K = 4
Property:	steps_min (exp-reward)

Invocation (default)

java -Xms10240m -Xmx10240m -jar ../epmc-standard.jar check --model-input-files consensus.4.prism --model-input-type prism --property-input-files consensus.props --property-input-names steps_min --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=4

Execution

Walltime:	4.956706285476685s
Return code:	0
Relative Error:	0.0002465025772942708

Log

assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property steps_min
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-done 43136 0
iterating
iterating-progress-unbounded 1847 6.346260850977269E-5 1
iterating-progress-unbounded 3809 1.3975138219809715E-6 2
iterating-done 4343 2
model-checking-done 4
command-check-result-is 767.810686020638 steps_min